System designers and engineers have continuously invented and employed methods and notations for modeling, specifying, simulating, verifying and controlling the designs of digital systems. As digital systems and, in particular, chips such as microprocessors and Application Specific Integrated Circuits (ASICs) have become more and more complex, with smaller feature sizes, and more components and functions employed on a single system or chip, function verification of integrated circuit design has become one of the most complicated and time consuming parts of the design process. In many cases, seventy percent, or more, of the design process is spent on functional verification of the design. To make matters worse, even when the considerable resources discussed above are dedicated to the functional verification of the design, there is still no guarantee that the resulting design will be error or “bug” free. Often, hidden bugs do not present themselves until late in the design process, even after tape-out of the design. This situation is particularly problematic since the later a bug appears, the harder it is to correct because any change in one part of the system inevitably affects another part of the system. Consequently, the later the bug is found, the more collateral subsystems are affected and the more complicated it is to fix.
In the prior art, two verification methods were widely accepted, the Simulation method and the Formal method, each having its own strengths and weaknesses relative to the other. The Simulation method is well known to those of skill in the art and has long been the verification method of choice because it is viewed as the simplest method and it can be employed to verify larger portions of a design under test, including a cluster, an entire system or an entire chip. The Simulation method relies on a set of test signals, called a test bench or test vector, which are fed into the design while the outputs and internal processing are monitored.
While easy to run, and the verification method of choice in the prior art, the Simulation method does not represent the most through or comprehensive test available and, therefore, is more susceptible to latent bugs that can present themselves late in the process; thereby creating the problems discussed above. For this reason, it is believed that, as integrated circuit systems become more complex, the Simulation method will become less used in favor of more robust and through verification methods.
The other verification method well known to those of skill in the art is the Formal method. The Formal method involves the use of mathematical models to theoretically, and exhaustively, verify the state space of a portion of the system under test. While the Formal method is the more comprehensive verification method, it has historically not been the method of choice for two reasons. First, historically, the Formal method could only be used on relatively small portions of the system and could not typically be used to verify an entire system such as a microprocessor in the whole. Consequently, to verify a complete system, the system had to be broken into a plurality of smaller parts, or “blocks” for use as the design under test. Second, the Formal method was difficult to formulate and involved the use of assertions and/or constraints. Assertions define certain behaviors and relationships of involved signals in a particular design being tested, or in the case of the Formal verification method as used in the prior art, a small portion of the entire system to be verified. Consequently, assertions had to be carefully crafted with great skill and considerable difficulty.
To make matters worse, in the prior art, each one of the plurality of blocks making up the system as a whole was verified separately, and often by different teams or individuals, and each block required its own set of assertions defined and used only in that block. As a result, not only was it extremely difficult to craft a proper set of assertions for any given block, but, in addition, each block had to have its own set of assertions created, often with significant redundancy. In addition, as systems became increasingly complex, using the Formal method, a given system needed to be broken down into more and more blocks. Consequently, while, in the prior art, the Formal method was recognized as the more robust and complete verification method, it was felt that the system as a whole, and the interaction of the various components of the system, could not be verified using the Formal method without prohibitive expense and use of resources.
A hybrid verification method, called Assertion Based Verification, combines the Simulation and Formal methods. Using Assertion Based Verification, Formal verification engines accept assertions as target properties to search or as constraint properties defining boundary conditions. The constraint assertions are then used as the assertions that define properties of a valid input for the Design Under Test (DUT). Using Assertion Based Verification, the Formal verification engine does not prove or disprove constraint assertions, but rather uses the constraint assertions to generate valid verification results. Consequently, using Assertion Based Verification, the target assertions are the design properties that the Formal verification engine tries to prove or disprove within the DUT.
Using Assertion Based Verification, once a design has been verified using the Formal method, the design is then still verified using the Simulation method. In this instance the assertions are used as monitors to find bugs in the Simulation and the assertions used as constraints in the Formal method are verified by the Simulation method. However, since, using prior art methods, assertions are often duplicated between DUTs, the Simulation method using these assertions as monitors results in redundant, contradictory and inefficient monitoring and reporting.
Since Assertion Based Verification, like the Formal method of verification, relied on, and was only as good as, carefully crafted assertions and constraints, Assertion Based Verification also suffered from the complexity, redundancy and complications associated with the Formal method discussed above.
Simulation, Formal, and Assertion Based Verification methods are well known to those of skill in the art, as are the strengths and weaknesses of each of these prior art methods. Consequently, a more detailed discussion of the Simulation, Formal and Assertion Based Verification methods is omitted here to avoid detracting from the invention. If the reader wishes a more detailed discussion of Simulation, Formal and Assertion Based Verification methods, the reader is referred to any one of numerous texts on the subject of verifiable RTL design. As one example, the reader is referred to “Principles of Verifiable RTL Design, A functional coding style supporting verification processes in Verilog” by Lionel Bening and Harry Foster, second edition, Kluwer Academic Publishers, Boston/Dordrecht/London, 2001, ISBN 0-7923-7368-5.
As noted above, in the both the Formal verification and the Assertion Based Verification methods of the prior art, the assertions must be carefully crafted, with great difficulty and, in the prior art, an assertion defined in one block or Design Under Test (DUT) was restricted to that DUT. Since as discussed above, using the prior art Formal or Assertion Based Verification methods, the DUT was typically a relatively small portion of the system as a whole, defining a set of assertions for the entire system, i.e., multiple DUT's, was prohibitively costly and difficult.
FIG. 1 shows a DUT_D that is a cluster of smaller DUTs such as DUT_A, DUT_B, and DUT_C. As noted above, Formal verification engines can typically only handle smaller size DUTs such as DUT_A, DUT_B, and DUT_C, but not larger, cluster or system size DUTs, such as DUT_D. As also noted above, this limited capacity of the Formal method results from the exhaustive nature of the analysis. Typically, these smaller DUTs, such as DUT_A, DUT_B, and DUT_C are called “block” level DUTs as opposed to cluster or “full-chip” level DUT_D. Unfortunately, the preferred level to build a simulation test environment is the cluster or “full-chip” level DUT_D because, as noted above, this provides information on block level interactions rather than individual block behavior. This is the primary reason the Simulation method was the method of choice in the prior art.
As noted above, to employ the Formal method or the Assertion Based Verification method, the verification must be performed on individual blocks DUT_A, DUT_B, and DUT_C, and not cluster block DUT_D. In addition, as also discussed above, in the prior art, assertions defined in any one of the individual blocks DUT_A, DUT_B, and DUT_C could only be used in that DUT and not in any of the other DUTs. Consequently, in the prior art, multiple sets of potentially redundant assertions had to be created.
As an example, in FIG. 1, assertions a1, a2 and a3 are defined in DUT_A and therefore regulate signals within the scope of DUT_A. Likewise, assertions b1, b2 and b3 are defined in DUT_B and therefore regulate signals within the scope of DUT_B and assertions c1, c2 and c3 are defined in DUT_C and therefore regulate signals within the scope of DUT_C. In addition, assertions d1, d2 and d3 are defined in DUT_D and therefore regulate signals within the scope of DUT_D. Consequently, using prior art Formal or Assertion Based Verification methods, assertions a1, a2, and a3 would be recognized for DUT_A and could act as either targets or constraints of DUT_A. However, using prior art methods, all other assertions b1, b2, b3, c1, c2, c3, d1, d2, and d3 were not involved when verifying DUT_A in DUT_A's environment because the signals used to define assertions other than a1, a2 and a3 were not considered part of DUT_A. Likewise, using prior art Formal or Assertion Based Verification methods, assertions b1, b2, and b3 were recognized for DUT_B and acted as either targets or constraints of DUT_B. However, using prior art methods, all other assertions a1, a2, a3, c1, c2, c3, d1, d2, and d3 were not involved when verifying DUT_B in DUT_B's. Likewise, using prior art Formal or Assertion Based Verification methods, assertions c1, c2, and c3 were recognized for DUT_C and acted as either targets or constraints of DUT_C. However, using prior art methods, all other assertions b1, b2, b3, a1, a2, a3, d1, d2, and d3 were not involved when verifying DUT_C in DUT_C's environment because the signals used to define assertions other than c1, c2 and c3 were not considered part of DUT_C. Finally, using prior art Formal or Assertion Based Verification methods, assertions d1, d2, and d3 were recognized for DUT_D and acted as monitors during simulation. All other assertions b1, b2, b3, c1, c2, c3, a1, a2, and a3 are included in DUT_D's simulation environment because they are within DUT_D.
As discussed above, assertions a1, a2, a3, b1, b2, b3, c1, c2, c3, d1, d2 and d3 define certain behaviors and relationships of involved signals in the particular design being tested, i.e., DUT_A, DUT_B, DUT_C and DUT_D, respectively. Consequently, assertions a1, a2, a3, b1, b2, b3, c1, c2, c3, d1, d2 and d3 had to be crafted with great care and significant energy and resources. However, as noted above, in the prior art, each one of the plurality of, DUTs making up the cluster DUT_D, i.e., DUT_A, DUT_B and DUT_C, was verified separately, in relative isolation, and often by different teams or individuals. As a result, not only was it extremely difficult to craft a proper set of assertions for any given DUT, such as DUT_A, DUT_B and DUT_C, but, in addition, each DUT had to have its own set of assertions created, often with significant redundancy and significant waste of time and resources.
In addition, as also noted above, as systems become more and more complex, using the Formal method, a given cluster DUT such as DUT_D needs to be broken down into more and more block DUTs, such as DUT_A, DUT_B and DUT_C. Consequently, as integrated circuit systems become more complex, the problem of redundancy of effort and resources using the prior art methods becomes even more pronounced.
In addition, all non-DUT specific assertions are logically connected to the DUT by design. Clearly it would be preferred to have information propagate automatically to all related DUT blocks, such as DUT_A, DUT_B and DUT_C in a given cluster and/or full chip system, such as DUT_D, in order to leverage all the development efforts of all the designers working on all the different DUTs. In the prior art, significant assertion re-use opportunities between blocks were missed and/or ignored. For instance, any assertion constraint for one DUT will naturally be a good target assertion for another DUT that generates related signals but this fact was ignored in the prior art.
The difficulty in individually defining the assertions for each DUT in the prior art has meant that the Formal method and Assertion Based Verification method of verification have largely been avoided in favor of the easier to implement, but less comprehensive, Simulation method. However, as integrated circuit systems have become increasingly complex the need for more exhaustive verification methods such as the Formal method and Assertion Based Verification method has become greater and greater.
What is needed is a method and apparatus for accelerating the development of assertions and for using assertions more efficiently, and with minimal redundancy to accelerate: the functional verification process, shorten the time-to-market period and improve the quality of design.